Nuprl Lemma : rv-disjoint_wf
11,40
postcript
pdf
p
:FinProbSpace,
n
:
,
X
,
Y
:RandomVariable(
p
;
n
). rv-disjoint(
p
;
n
;
X
;
Y
)
latex
Definitions
RandomVariable(
p
;
n
)
,
rv-disjoint(
p
;
n
;
X
;
Y
)
,
P
Q
,
left
+
right
,
P
Q
,
A
,
,
,
s
=
t
,
f
(
a
)
,
Type
,
{
i
..
j
}
,
#$n
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
Outcome
,
x
:
A
.
B
(
x
)
,
,
,
t
T
,
FinProbSpace
Lemmas
finite-prob-space
wf
,
nat
wf
,
rationals
wf
,
p-outcome
wf
,
int
seg
wf
,
not
wf
origin
p:FinProbSpace, n:
, X, Y:RandomVariable(p;n). rv-disjoint(p;n;X;Y) 
p:FinProbSpace, n:, X, Y:RandomVariable(p;n). rv-disjoint(p;n;X;Y) 
Q
Q
A
}
B(x)x:A. B(x)
T